\section{Statements and Expressions}

\subsection{Exceptions}

Several places below  refer to an exception being thrown.
The semantics of an exception being thrown is that the application
halts with a run-time error.  Future versions of this document will
define facilities for propagating and catching exceptions.


\subsection{Statements}

Several locations in this document refer to an exception being thrown.
The semantics of an exception being thrown is that the application
halts with a run-time error.  Future versions of this document will
define facilities for propagating and catching exceptions.


\TODO{discuss field/method unification}

\begin{quote}
\ntermdef{Stmt}

\defspace \nterm{Expr}

\defspace \nterm{VarDecl}


\ntermdef{VarDecl}

\defspace \nterm{Specifier} \vII{\opt{\nterm{Type}}} \nterm{Identifier} = \nterm{Expr}


\ntermdef{Specifier}

\defspace \keyw{val}

\defspace \keyw{var}

\end{quote}

Statements are either expressions, or variable declarations.  A
variable declaration must include an initial value.  Variables can be
declared with the \keyw{val} or \keyw{var} keyword; the former
indicates an immutable let binding, whereas the latter indicates a
mutable variable that can be reassigned later.

\vII{An optional type may be given for variable declarations.  If the type
is omitted, then it is inferred to be the
same as the initializing expression.}

Statements evaluate to values, based on the expression in the
statement or the value of the initializer for the variable.  The last
statement in a sequence is used for the return value of a method or
the result of a block.

\subsection{Expressions}

\begin{quote}

\ntermdef{Expr}

%\defspace \keyw{return} FnExpr

%\defspace FnExpr

%\end{quote}

%The \keyw{return} construct returns from the nearest lexically
%enclosing method.

%\begin{quote}

%\ntermdef{FnExpr}

\defspace \keyw{fn} (\opt{\nterm{Args}})
              \vII{\opt{[\nterm{Args}]}}
              => \nterm{Expr}

\defspace \nterm{Expr1}

\end{quote}

A first-class function.  \vII{The optional arguments surrounded with
  [] support specifying types and permissions for variables that are
  currently in scope, along with any state changes made to these
  variables.}

\begin{quote}

\ntermdef{Expr1}

\defspace \opt{\nterm{SimpleExpr} .} \nterm{Identifier} = \nterm{Expr}

\defspace \nterm{SimpleExpr} <- \nterm{State}

\defspace \keyw{match} ( \nterm{InfixExpr} ) \{ \seq{CaseClause} \}

\defspace \nterm{InfixExpr}

\end{quote}

The assignment form is for fields or for already-declared local
variables, which must have been declared using \keyw{var}.  If the
identifier being assigned does not match a locally declared variable,
and no qualifier is specified, then it is assumed to be an assignment
to an already-declared field of the current object \keyw{this}.
\pII{All assignments to a field \code{f} are really syntactic sugar
  for calling a setter function \code{setF}.}

The state change operator <- modifies the object to the left of the
arrow as follows:

\TODO{The semantics of state change are based on the notion of
  \textit{tags} as defined below and used for pattern matching.  We
  first determine which tags are added and removed.  New tags are
  added when they are associated with states referenced to the right
  of the operator.  We say two tags are \textit{inconsistent} if they
  are (transitively) different cases of the same state.  If any of the
  new tags are inconsistent with any old tag, that old tag is removed.
  Other old tags are retained.  All members that were declared or
  required in tags that are removed, and are not declared or required
  by any tags being retained, are removed from the object.  All other
  old members are retained, unless they have the same name as those on
  the right, in which case those on the right override them.  \pII{If
    this results in a member being incompatible with an abstract
    member of a remaining tag, an \code{IllegalStateChangeException}
    is thrown.}  Finally, all members on the right are added to the
  object.}

\TODO{At some point, consider whether to support matching against
structural types}

\begin{itemize}

\item
All old members of the object are removed.  In addition to members,
objects have \textit{tags} (as defined below) in order to support pattern
matching; all old tags of the object are also removed.

\item
All tags from states referenced on the
right of the operator are added to the object.

\item
All members on the right are added to the object.

\end{itemize}

\vII{The type of the state change operation is \texttt{void}}

\TODO{allow specifically keeping or removing individual members and
tags}

\TODO{extend the above so that fields defining type members (or module
members that might define types) are always kept in the object}

\openi{Integrate dimensions, as in ``change only in this dimension.''
  Specify that data that will never be accessed again is garbage
  collected.}

\openi{Should we support a history notation where we restore previous
field values when we re-enter a state?}

\openi{what if you transition to a state that has an identically named
  field or method but that is not inherited from a common supertype?
  Can the field from the former state fill in for the field from the
  new state? Or do I have to redefine it?}

The \keyw{match} expression matches an input expression to one of
several cases using the \nterm{CaseClause} construct defined below.
The overall match expression evaluates to whatever value the
chosen case body evaluates to.

\begin{quote}

\ntermdef{CaseClause}

\defspace \keyw{case} \nterm{Pattern} \nterm{BlockExpr}

\defspace \keyw{default} \nterm{BlockExpr}

\ntermdef{Pattern}

\defspace \nterm{QualifiedIdentifier} \opt{\nterm{Identifier}} \pII{\nterm{Identifier}}

\pII{\defspace \nterm{InfixExpr}}

%\defspace \keyw{default}


\ntermdef{QualifiedIdentifier}

\defspace \nterm{Identifier} \seq{ . \nterm{Identifier}}

\end{quote}

The value is matched against each of the cases in order.  For the
first case that matches, the corresponding expression list is
evaluated.  If no pattern matches, a \code{NoMatchException} is
thrown.

The first kind of pattern syntax tests the value's tags against
the \nterm{QualifiedIdentifier} given.  The match succeeds if
one of the tags of the value is equal to the tag
\nterm{QualifiedIdentifier}, or if one of the tags of the value
was declared in a state that is a transitive case of the
\nterm{QualifiedIdentifier} specified.

The \nterm{QualifiedIdentifier}
must resolve to a state declared with the \keyw{case} \keyw{of}
construct; otherwise, a \code{IllegalCaseException} is
thrown.  If the
match is successful, the matched value is bound to the
\nterm{Identifier} given in the expression body.

\pII{The second kind of pattern syntax tests for equality with a
  value.}  For the default pattern, the match always succeeds.  If
there is a default pattern, it must be the last one in the match
expression.

\TODO{more interesting patterns, including tuples, structural matching,
value matching}

\begin{quote}

\ntermdef{InfixExpr}

\vI{\defspace \nterm{SimpleExpr}}

\vII{\defspace \nterm{CastExpr}}

\defspace \nterm{InfixExpr} \nterm{IdentifierOrOperator} \nterm{InfixExpr}


\ntermdef{IdentifierOrOperator}

\defspace \nterm{Identifier} \alt \nterm{Operator}


\vII{\ntermdef{CastExpr}}

\vII{\defspace \nterm{SimpleExpr} \opt{\keyw{as} \nterm{Type}}}

\end{quote}

The operators defined in Java have the same precedence in Plaid as
they do in Java.  Identifiers as well as symbolic operators can be
used as infix operators; both are treated as method calls on the
object on the left of the operator.  Non-Java operators and
identifiers used as infix operators have a precedence above assignment
and state change, and below all other operators.

\vII{Cast expressions assert that a variable has a given type, and
also assert the relevant permission for that variable.  If it is
determined that the variable does not have that type, or that the
permission being asserted is in conflict with other permissions on
the stack or in the heap, the cast may fail with an exception.
Implementations are not required to detect the cast failure
immediately; they may throw an exception later that ``blames''
the failed cast.}

\TODO{Define the above more precisely.  Place constraints on when
the cast can fail.}

\begin{quote}

\ntermdef{SimpleExpr}

\defspace \nterm{BlockExpr}

\defspace \keyw{new} \nterm{State}

\defspace \nterm{SimpleExpr2}

\pII{\defspace ( \nterm{Type} ) \nterm{SimpleExpr}}

\end{quote}

The \keyw{new} statement creates an object initialized according to
the \nterm{State} specification given (defined below).  The object
creation and field assignment is done atomically; there is never a
``partially initialized'' object.

\pII{The cast expression casts the value to the given permission type,
throwing an exception if the cast does not succeed.  The cast checks
if the given permission kind is compatible with existing permissions
that are live in the heap.  It also checks whether the object has all
the members and tags associated with the state given.
\openi{The cast construct should not be a way to violate encapsulation;
so it should not expose members or tags that were deliberately hidden
(as opposed to just passing to a Dynamic type).}}

\begin{quote}

\ntermdef{BlockExpr}

\defspace \{ \nterm{StmtListSemi} \}

\ntermdef{StmtListSemi}

\defspace \nterm{Stmt} \seq{ ; \nterm{Stmt}} \opt{;}

\end{quote}

Block expressions have a semicolon-separated list of statements, with
an optional semicolon at the end.  The statement list evaluates to the
value given by the last statement in the list.

\begin{quote}

\ntermdef{SimpleExpr2}

\defspace \nterm{SimpleExpr1}

\defspace \nterm{SimpleExpr2} \nterm{BlockExpr}

\end{quote}

To enable control structures with a natural, Java-like syntax, we allow
a function to be invoked passing a block expression as an argument.  The
block expression is essentially a zero-argument lambda.

\begin{quote}

\ntermdef{SimpleExpr1}

\defspace \nterm{Literal}

\defspace \nterm{Identifier}

\defspace \keyw{this}

\defspace ( \nterm{ExprList} )

\defspace \nterm{SimpleExpr1} . \nterm{Identifier}

\defspace \nterm{SimpleExpr1} \nterm{ArgumentExpr}

\ntermdef{ExprList}

\defspace \nterm{Expr} \seq{ , \nterm{Expr}}

%\ntermdef{ArgumentExprs}

%\defspace \nterm{ArgumentExpr} \seq{\nterm{ArgumentExpr}}

\ntermdef{ArgumentExpr}

%\defspace \nterm{BlockExpr}

\defspace (  \nterm{ExprList} )

\end{quote}

Parenthesized expressions can in fact be a list of expressions,
supporting easy tuple construction.%\pI{ (supported in Phase II of Plaid only)}.

\pII{As with field assignment, dereferencing a field \code{f} is syntactic
sugar for calling a getter method \code{getF}.}

As in Scala, multiple argument expressions can be given at a call
site, supporting currying.  An argument expression is a
traditional parenthesis-surrounded expression list.


\TODO{Add XML expressions}

\section{Declarations}

\begin{quote}
\ntermdef{Decl}

\defspace \vII{\seq{\nterm{Modifier}}} \keyw{state} \nterm{Identifier}
          \opt{\keyw{case} \keyw{of} \nterm{QualifiedIdentifier}}
          \pII{\opt{\keyw{comprises} \nterm{QualifiedIdentifierList}}}
          \opt{\nterm{StateBinding}} \opt{;}

\pII{\defspace \seq{\nterm{Modifier}} \keyw{interface} \nterm{Identifier}
          \opt{\keyw{case} \keyw{of} \nterm{QualifiedIdentifier}}
          \opt{\keyw{comprises} \nterm{QualifiedIdentifierList}}
          \opt{\nterm{StateTypeBinding}}}

\pII{\defspace \seq{\nterm{Modifier}} \keyw{type} \nterm{Identifier}
          \opt{\nterm{TypeDef}}}

\defspace \seq{\nterm{Modifier}} \nterm{MSpec} ;

\defspace \seq{\nterm{Modifier}} \nterm{MSpec} \nterm{BlockExpr}

\defspace \seq{\nterm{Modifier}} \nterm{FieldDecl} ;


\end{quote}

\keyw{state} declarations specify the implementation of a state,
as specified in the state definition.

\pII{\keyw{state} declarations specify both an interface and an
implementation.  The interface is referenced by \nterm{Identifier};
the implementation by \nterm{Identifier}.impl.  An \keyw{interface}
declaration is identical except that it just defines a type.
\keyw{state} declarations are bound to a state definition, whereas
\keyw{interface} declarations are bound to an interface definition.}

The \keyw{case} \keyw{of} construct means that this state is given its
own \textit{tag} that can be used to test whether objects are in
that state.  Only states declared with \keyw{case} \keyw{of} can
be given in a pattern for a case in a \keyw{match} statement.
Different cases of the same superstate are orthogonal; no object may
ever be tagged with two cases of the same superstate.

\pII{The \keyw{comprises} construct means that every instance of this state
or interface must be tagged with one of the states listed.  It is an
error to instantiate an object of the superstate without tagging it
with one of the substates.  It is also an error to declare some state
a case of this state unless it is listed in the comprises clause.
Conversely, it is an error to list a state in the comprises clause
unless that state is a case of this state.}

\pII{The \keyw{type} declaration declares a name for a type, including any
corresponding permission.  The type definition syntax is given below.}

The final two cases are for method and field declarations.  The
method declaration has \pI{a method header} \pII{one or more method headers \nterm{MSpec}} and an
optional method body.  \pII{If there is more than one method header it
means that the method has the intersection of the types implied by all
of the headers; for example, it may make one state transition if the
receiver is in one state but another transition if the receiver is in
another state, and the only way to specify this in a Java-like syntax
is to have two complete method headers.}  If the body is missing then
the method is abstract and may be filled in by sub-states or when the
state is instantiated.

Fields are discussed in more detail below.

\TODO{need static methods--bad!}

\begin{quote}

\ntermdef{StateBinding}

\pII{\defspace <: \nterm{StateType}}

\defspace = \nterm{State}

\defspace \{ \seq{\nterm{Decl}} \}

\end{quote}

\pII{As in virtual types or type members, states can be given a precise
definition or can be bound by a supertype.  If only a bound is given,
substates can give tighter bounds or an actual definition.  Some
definition must be given before instantiating the state.}

\begin{quote}

\ntermdef{State}

\defspace \nterm{StatePrim} \seq{\keyw{with} \nterm{StatePrim}} % left-associative

\ntermdef{StatePrim}

\defspace \nterm{SimpleExpr1}  %\opt{<\nterm{PermBindingList}>} \opt{\{ \nterm{RenameList} \}}
\opt{\{ \seq{\nterm{Decl}} \}}

\defspace \{ \seq{\nterm{Decl}} \}

\end{quote}

A state is a composition of primitive states separated by the
\keyw{with} keyword.  These primitive states can be literal blocks
with a series of declarations, or they can be references to some
previous object or state definition.

Composition is in general symmetric, as in traits.  It is an error if
more than one state defines a member, unless one of the primitive
states is a block and the member is given the \keyw{overrides}
modifier there.  \pII{To avoid these errors, it is possible to rename,
alias, or hide members from one of the composed states, as described
below.}

%Composition of states is not supported in Phase I of Plaid, nor is
%renaming, aliasing, or hiding.

\openi{Map<K,V> syntactic sugar}

%\begin{quote}

%\ntermdef{PermBindingList}

%\defspace \nterm{Type} \seq{ , \nterm{Type}}

%\ntermdef{PermBinding}

%\defspace \opt{\nterm{Identifier} =} \nterm{Type}

%\end{quote}


\pII{When a state is specified, any required type members can be bound
  with a syntax similar to generics in languages like C++, C\#, or
  Java.  Type member declarations, unlike fields in many languages,
  are ordered, so that the syntax \code{C<S,T,U>} binds the first type
  member of C to S, the second member to T, and the third to U.  If
  state C has type members \code{s}, \code{t}, and \code{u}, the code
  above is equivalent to \code{C \keyw{with} \{ \keyw{type} s = S;
    \keyw{type} t = T; \keyw{type} u = U; \}}}

%It is
%also possible to specify some type members by name, as in
%\code{C<W,t=S,u=V>}.  To avoid ambiguity, once a type member has been
%specified with the '=' syntax, all subsequent type member
%specifications mus also use '=' (rather than ordering).

%\begin{quote}

%\ntermdef{RenameList}

%\defspace \nterm{RenameOp} \seq{ , \nterm{RenameOp}}

%\ntermdef{RenameOp}

%\defspace \nterm{Identifier} -> \nterm{Identifier}  % alias

%\defspace \nterm{Identifier} ->- \nterm{Identifier} % rename

%\defspace - \nterm{Identifier} % remove

%\defspace ? \nterm{Identifier} % make required

%\end{quote}

\pII{The -> operator makes the name on the left an alias to the member on
the right.  The unary - operator removes the specified member.  The
->- operator is a rename, which can be viewed as a combination of
these: it aliases and then removes the member on the right.
%
The ? operator means the specified member is required (even though it may
not have been specified with the \keyw{requires} keyword in the base
interface).  This operator cannot be applied to states; it is used to
modify the types of interfaces (i.e. in a \nterm{StateTypePrim}, below, not
a \nterm{StatePrim}).
%
Through either an overrides declaration, or a rename or remove followed
by a redefinition, it is possible to replace an existing member of a
state with another.  References to that member in code defined in the
state still refer to the old member, however, unless that member was
marked \keyw{open} (for open recursion).  However, any references to
the member through variables, including \keyw{this}, are redirected to
the new member.
%
\TODO{consider a different syntax for - and with for types (and maybe
for ? too), to distinguish them from composition operators on objects.
see Eric's emails 10/10/09}
}


\begin{quote}


%%%%%%%%%%%%%%%%%% Fields and Methods %%%%%%%%%%%%%%%%%%%%%

\ntermdef{FieldDecl}

\defspace \nterm{ConcreteFieldDecl}

\defspace \nterm{AbstractFieldDecl}

\ntermdef{ConcreteFieldDecl}

\defspace \opt{\nterm{Specifier}} \vII{\opt{Type}} \nterm{Identifier} = \nterm{Expr}

\ntermdef{AbstractFieldDecl}

\defspace \pII{\seq{\nterm{Modifier}}} \nterm{Specifier} \vII{\opt{Type}} \nterm{Identifier}



\ntermdef{MSpec}

\defspace \keyw{method} \vII{\opt{\nterm{Type}}} \nterm{IdentifierOrOperator} ( \opt{\nterm{Args}} )
          \vII{\opt{[ \opt{\nterm{ArgSpec} \opt{\keyw{this}}}, \opt{\nterm{Args}}]}}

\pII{
\defspace \nterm{ReturnSpec} \nterm{IdentifierOrOperator} ( \nterm{Args} )
          \opt{[ \nterm{Args}]}
%
\ntermdef{ReturnSpec}
%
\defspace \keyw{method}
%
\defspace \nterm{Type}
}

\ntermdef{Args}

\vI{\defspace \nterm{Identifier} \seq{ , \nterm{Identifier}}}
\vII{\defspace \opt{\nterm{ArgSpec}} \nterm{Identifier} \seq{ , \opt{\nterm{ArgSpec}} \nterm{Identifier}}}

\vII{\ntermdef{ArgSpec}}

\vII{\defspace \nterm{Type} \opt{$>>$ \nterm{Type}}}

\end{quote}

The \nterm{FieldDecl} form should be familiar from Java-like
languages.  If no expression is given then the field is abstract.  All
fields can only be assigned from within the
state. \pII{, but getter and setter methods are automatically defined
  for the FieldDecl if they are not otherwise specified in the state,
  and the visibility specifier on the field is applied to the getter
  and setter.}
When fields are first defined a specifier (\keyw{var} or \keyw{val})
must be given; later, when the field is overridden and given a concrete
value, the specifier must be omitted.
\keyw{var} fields are mutable, \keyw{val} fields
are not\pII{ (i.e. no setter is defined)}.

Field initialization expressions are run in the order given;
initializers are run even if a field is overridden.  Fields defined
earlier are in scope during the execution of a field initializer.
If the field initializer is run from inside a constructor, the
object ``this'' being constructed is not in scope, as it will not
even be created until all field initializers are run.  If the field
initializer is run from a state change operation, then the old ``this''
object is in scope, with whatever permissions are available in the
context.  In the case of state update an expression of the form ``this.f''
refers to the old value of a field, while ``f'' refers to the new value
if ``f'' has been re-initialized already, otherwise the old value.


\vII{If a type is missing and an expression is given for a
  \keyw{val} field, then the type of the field is inferred from the
  expression.  If the type is missing and either no expression is
  given or it is a \keyw{var} field, then the type is \keyw{dynamic}.}

The method header \nterm{MSpec} also has a standard format. If the return type is missing, then the type is \keyw{dynamic}. The square brackets contain optional permissions and state changes to variables in scope . Permissions to the receiver can be specified by an \nterm{ArgSpec} with or without the \keyw{this} keyword. If no permission to the receiver is given, the \nterm{PermKind} modifier on the state declaration is used, or \keyw{dynamic} if there is no \nterm{PermKind} modifier. All other variables in scope needed by the method are specified  with \nterm{Args}.

\vII{Each argument specification includes a permission, but if a different
permission is returned this can be indicated with a $>>$ and the new
permission.}

\TODO{generalize the tuple construct so it can be used for more than method
arguments}

It is an error to have two methods, two fields, or a method and a
field with the same name, unless one of the two has the ``overrides''
keyword.

\begin{quote}

%%%%%%%%%%%%%%%%%% Modifiers %%%%%%%%%%%%%%%%%%%%%

\ntermdef{Modifier}

\vII{\defspace \keyw{requires}}

\defspace \keyw{overrides}

\vII{\defspace \keyw{branded}}

\vII{\defspace \nterm{PermKind}}

\pII{
%
\defspace \keyw{concrete} \opt{:\nterm{QualifiedName}}
%
\defspace \keyw{open}
%
\defspace \keyw{impl}
%
\defspace \nterm{QualifiedName} :
%
\defspace \keyw{public} \opt{:\nterm{QualifiedName}}
%
\defspace \keyw{protected}
%
\defspace \keyw{private}
%
\defspace \keyw{static}
%
\defspace \keyw{conserved}
}

%\defspace \keyw{const}

%\defspace \keyw{byname}

\end{quote}

%const - returns same thing every time the field is dereferenced or the
%function is called

\keyw{overrides} indicates that a method overrides a function of the
same name during composition.

\vII{\keyw{branded} indicates that the type being defined is nominal, and
is a (strict) subtype of the structural type given by its signature.
If one state is a case of another, both states must be \keyw{branded}.}

\vII{\keyw{requires} is similar to \keyw{abstract} in Java.  However,
things are more interesting in Plaid, because one can pass around an
object that has abstract/required members.  It is not necessary to
use the \keyw{requires} modifier in state definitions; one can simply
leave off the definition of a function.  \keyw{requires} is necessary
in types, however, to distinguish the presence vs. absence of a
member in that type.  Unlike in Java, methods may be called on an
object that has a required member, but only if the type given to the
method's receiver does not expect that member to be present.}
\pII{, and so we have to be able
to describe its type.  In particular, that type does not have the
required members, but all of the methods by default (i.e. unless
otherwise specified) require the receiver to have all of those members
defined.}

\vII{If a \nterm{PermKind} is specified than any variables
in that state have the specified permission by default. In addition,
the \keyw{this} parameter to methods of this state will have the
specified permission by default. }

\pII{
%
open - references to this function in the current state should be
re-bound if state is composed with another that overrides this
function. \openi{what about explicit calls on this vs. implicit calls?}
%
The visibility modifiers are ignored in Plaid Phase I
%
\TODO{Define static in terms of a rewriting into an object for the
static state and a prototype object}
%
\keyw{byname} means pass by name: the argument is automatically
closure-converted and the closure is evaluated on each use of the
formal argument.
%
\keyw{conserved} means a permission can be duplicated without
losing precision.
%
\nterm{QualifiedName} : indicates a data group.
%
\keyw{impl} means use the abstract data type specific to a single
implementation, as opposed to just the structural public type
declared.
%
concrete means may be instantiated (no hidden abstract members).
The optional annotation shows how far the concrete annotation
propagates; outside the given scope the state is not known to be
concrete.
%
Note: if we inherit a tag then any members associated with that tag that might
be removed (with ``-'') must be added back in.
%
Whoops--two different meanings of @!
}

\TODO{Refine definitions}

\TODO{Later add delegation, maybe requires}

\openi{Should we call Perm a Type, made up of a Permission and a State?}

%\begin{verbatim}
%
%
%modifier ::= concrete [:QualifiedName] // on a state, means "can be instantiated from outside this state (or concrete within the QualifiedName package tree)"
%                      // (typically not concrete because requires fields/methods are hidden)
%         |   requires // on methods, fields, and types
%	 |   const // C++ const for fields, except real const; for methods, means it's a pure function
%	 |   public [:QualifiedName] // visible globally, or inside QualifiedName
%	 |   protected // question: Java semantics or C++ semantics?  Probably C++
%	 |   private
%         |   static // for factory methods
%	 |   conserved	// only on permissions
%
%\end{verbatim}
%
%permkind ::= unique
%	 |   full
%	 |   shared
%	 |   pure
%	 |   immutable
%	 |   none	// for a permission that gets captured
%Perm	::= [permkind] State[@State]
%	|   argspecs | args -> Perm		//argspecs are *-delimited
%	|   QualifiedIdentifier
%	|   (Perm)			// parenthesis
%	|   Perm * Perm			// tuples
%
%arg	::= argspec Identifier
%
%argspec ::= Perm [>> Perm]
%
%decl	::= modifiers mspecs [{ exp }]
%	|   modifiers Perm Identifier [ = exp]	// fields
%	|   modifiers state Identifier [statedef]
%	|   modifiers type Identifier [permdef]
%
%permdef ::= = Perm
%	|   <: Perm
%
%mspec	::= Perm Identifier(args [| args])
%
%statedef ::= = State
%	 |   <: State
%	 |   [extends State] [comprises States] { decls }		// later: add delegation, maybe requires
%

\TODO{may need to add fractions}

\TODO{Read Scharli ECOOP '04 paper on encapsulation policies}

\TODO{Metadata/annotations}

\TODO{Javadoc}

\TODO{add an LL(1) grammar to the spec as a reference}

\pII{
\section{Concurrency}
%
\TODO{nice synch mechanism suggested by Nick Cameron (FTfJP06) -
  concurrent call can wait until object is in a state}
%
\section{Visibility}
%
By default members are visible throughout the surrounding package.
The \keyw{private} modifier makes them visible only in the surrounding
scope.  The \keyw{protected} annotation makes them visibile in
subclasses (and unlike Java, not in the surrounding package).  The
\keyw{public} modifier makes them globally visible by default, but if
the \keyw{public} modifier is given an argument then the member is
visible within that argument but not outside.
%
Members cannot be hidden as in Java/C++; overriding a member with one
of an incompatible type is an error.
%
\TODO{Will need dynamic notion of sealing if we have gradual or
  dynamic typing.  Research topic in higher-order module setting.}
%
\section{Inheritance}
%
All fields in non-final states must be requires or const.  Rationale:
makes everything that you inherit from just an interface, possibly
with reusable code.  If you want to reuse something stateful, use
composition not inheritance.  Const==const as long as we're in this
state.  Question: should we require not just const, but also immutable?
%
Static methods are not inherited.  Semantically, static methods are
just instance members of the enclosing module, which happen to have
privileged access to the class.  [Question: what does this mean from a
  compilation/translation point of view?  Maybe this is not the right
  interpretation.]
%
Possible relaxation: no assignment to private fields.  Rationale:
white-box inheritance is easier to reason about, and if you want
black-box composition you should use composition.
%
Selective Open Recursion.  Methods that are callbacks to substates
should be marked open.  Implicit calls to this will be statically
dispatched to the same (static) class, not the dynamic class, unless
the method is marked open.  Explicit calls to this will be dynamically
dispatched, but the compiler will give a warning that the method
should be marked open.  Rationale: callback-based design intent should
be explicit.  Permission to this must be packed before calling an open
method.
}


